/* test tree
NOTE: not yet finished the assertion here for assertion language's limited expressive power
*/
struct tree{
  int data;
  struct tree * l;
  struct tree * r;
};

bool successful;
/*@ let  tree(t) = t==null ||
  	({{t}}&&tree(t->l)&&tree(t->l))
    in tree(t)&& (f==null || (f!=null) && (f->l==t|| f->r==t))
    end
*/
struct tree *  SearchBST(struct tree * t, int key, struct tree * f)
{
	struct tree * q;
	if(t==null)
	{
		q = f;
		successful = false;
		return q;
	}
	else if(key== t->data)
	{
		q = t; 
		successful = true;
		return q;
	}
	else if(key <= t->data)
	{
		q = SearchBST(t->l,key,t);
		return q;
	}
	else
	{
		q = SearchBST(t->r,key,t);
		return q;
	}
}
/*@tree(t)*/